es:ES, e, e', a, b:E. a before b  [e, e']  (a <loc b) & e  a  & b  e'  

latex

Definitions	t  T, x:A. B(x), e  e' , Prop, P & Q, (e <loc e'), E, P  Q, False, P  Q, P  Q, P  Q, x before y  l, before(e), (x  l), as @ bs, es-ble{i:l}(es;e;e'), b, filter(P;l), [e, e'], ES, {T}, Trans x,y:T. E(x;y)
Lemmas	es-le-trans, event system wf, l before filter, filter wf, assert-es-ble, assert wf, es-ble wf, l before append iff, append wf, member singleton, l before-es-before-iff, member-es-before, l member wf, es-before wf, iff functionality wrt iff, and functionality wrt iff, or functionality wrt iff, singleton before, l before wf, false wf, es-E wf, es-locl wf, es-le wf